Nuprl Lemma : eventtype_wf
0,22
postcript
pdf
E
:Type,
V
:(Id
Id
Type),
M
:(IdLnk
Id
Type),
loc
:(
E
Id),
k
:(
E
Knd),
e
:
E
.
eventtype(
k
;
loc
;
V
;
M
;
e
)
Type
latex
Definitions
eventtype(
k
;
loc
;
V
;
M
;
e
)
,
P
Q
,
Knd
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
islocal(
k
)
,
act(
k
)
,
lnk(
k
)
,
tag(
k
)
,
1of(
t
)
,
2of(
t
)
,
Id
,
IdLnk
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
pi2
wf
,
Id
wf
,
IdLnk
wf
,
pi1
wf
,
Knd
wf
origin
E:Type, V:(Id
IdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), e:E.
Type E:Type, V:(IdIdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), e:E.
Type 
Q
x. t(x)x:A. B(x) T